A:Type, f, g:a:A fp Top, eq:EqDecider(A), x:A.
(x  fpf-domain(f  g))  (x  fpf-domain(f))  (x  fpf-domain(g)) 

latex

Definitions	t  T, Top, x.A(x), x:A. B(x), x. t(x), P  Q, P  Q, P & Q, P  Q, Type, a:A fp B(a), EqDecider(T), f  g, x  dom(f), b, {T}, P  Q, x:AB(x), left+right, fpf-domain(f), (x  l), Prop, x:AB(x)
Lemmas	iff functionality wrt iff, fpf-join-dom, l member wf, fpf-domain wf, assert wf, fpf-dom wf, deq wf, fpf wf, member-fpf-domain, fpf-join wf, top wf